\begin{tabbing}
$\forall$\=${\it loc}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it knd}$:Knd, $T$:Type, $x$:Id,\+
\\[0ex]$f$:((State(${\it ds}$)$\rightarrow$$T$$\rightarrow$DeclaredType(${\it ds}$;$x$)) + (State(${\it ds}$)$\rightarrow$$T$$\rightarrow\mathbb{Q}\rightarrow$DeclaredType(${\it ds}$;$x$))).
\-\\[0ex]R{-}Feasible(Reffect(${\it loc}$;${\it ds}$;${\it knd}$;$T$;$x$;$f$)) $\Rightarrow$ ($\uparrow$$x$ $\in$ dom(${\it ds}$))
\end{tabbing}